$\forall$$T$:Type, $l$:($T$ List), $i$:\{0..$\parallel$$l$$\parallel^{-}$\}, $j$:\{0..$i$$^{-}$\}. last(l\_interval($l$;$j$;$i$)) = $l$[($i$ {-} 1)] $\in$ $T$